rx, ra, rt:(IdId), M:MsgA.
Inj(Id; Id; rx)  Inj(Id; Id; ra)  Inj(Id; Id; rt)  ma-rename(rx;ra;rt;M)  MsgA 

latex

Definitions	x:A. B(x), P  Q, t  T, ma-rename(rx;ra;rt;M), mk-ma, 1of(t), 2of(t), x. t(x), State(ds), f o g, Prop, Valtype(da;k), locl(a), kind-rename(ra;rt;k), kindcase(k; a.f(a); l,t.g(l;t) ), if b t else f fi, islocal(k), act(k), b, isl(x), outr(x), true, false, S  T, rcv(l,tg), lnk(k), tag(k), outl(x), MsgA, x(s), Id, Knd, Inj(A; B; f)
Lemmas	mk-ma wf, fpf-rename wf, Id wf, id-deq wf, Knd wf, Kind-deq wf, kind-rename wf, IdLnk wf, inject wf, msga wf, fpf wf, fpf-cap wf, subtype rel self, deq wf, fpf-rename-cap, fpf-compose wf, fpf-rename-cap3, top wf, locl wf, kind-rename-inj, subtype-fpf3, strong-subtype-self, ma-state wf, pi1 wf, rcv wf, pi2 wf, map wf, ma-valtype wf, product-deq wf, idlnk-deq wf